(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(a, f(b, x)) → f(a, f(a, f(a, x)))
f(b, f(a, x)) → f(b, f(b, f(b, x)))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(a, f(b, z0)) → c(F(a, f(a, f(a, z0))), F(a, f(a, z0)), F(a, z0))
F(b, f(a, z0)) → c1(F(b, f(b, f(b, z0))), F(b, f(b, z0)), F(b, z0))
S tuples:
F(a, f(b, z0)) → c(F(a, f(a, f(a, z0))), F(a, f(a, z0)), F(a, z0))
F(b, f(a, z0)) → c1(F(b, f(b, f(b, z0))), F(b, f(b, z0)), F(b, z0))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c, c1
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
b,
z0)) →
c(
F(
a,
f(
a,
f(
a,
z0))),
F(
a,
f(
a,
z0)),
F(
a,
z0)) by
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(a, f(b, x0)) → c
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(b, f(a, z0)) → c1(F(b, f(b, f(b, z0))), F(b, f(b, z0)), F(b, z0))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(a, f(b, x0)) → c
S tuples:
F(b, f(a, z0)) → c1(F(b, f(b, f(b, z0))), F(b, f(b, z0)), F(b, z0))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(a, f(b, x0)) → c
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c, c
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(a, f(b, x0)) → c
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(b, f(a, z0)) → c1(F(b, f(b, f(b, z0))), F(b, f(b, z0)), F(b, z0))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
S tuples:
F(b, f(a, z0)) → c1(F(b, f(b, f(b, z0))), F(b, f(b, z0)), F(b, z0))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
b,
f(
a,
z0)) →
c1(
F(
b,
f(
b,
f(
b,
z0))),
F(
b,
f(
b,
z0)),
F(
b,
z0)) by
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
F(b, f(a, x0)) → c1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
F(b, f(a, x0)) → c1
S tuples:
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
F(b, f(a, x0)) → c1
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c, c1, c1
(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(b, f(a, x0)) → c1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
S tuples:
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, f(a, z0))))), F(a, f(a, f(b, z0))), F(a, f(b, z0)))
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c, c1
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
b,
f(
b,
z0))) →
c(
F(
a,
f(
a,
f(
a,
f(
a,
f(
a,
z0))))),
F(
a,
f(
a,
f(
b,
z0))),
F(
a,
f(
b,
z0))) by
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(b, f(b, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(b, f(b, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
S tuples:
F(b, f(a, f(a, z0))) → c1(F(b, f(b, f(b, f(b, f(b, z0))))), F(b, f(b, f(a, z0))), F(b, f(a, z0)))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(b, f(b, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c, c
(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
b,
f(
a,
f(
a,
z0))) →
c1(
F(
b,
f(
b,
f(
b,
f(
b,
f(
b,
z0))))),
F(
b,
f(
b,
f(
a,
z0))),
F(
b,
f(
a,
z0))) by
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(b, f(b, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
S tuples:
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(b, f(b, z0)))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c, c, c1, c1
(15) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(b, f(b, z0)))), F(a, f(b, f(b, z0)))) by F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
S tuples:
F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0))))
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c, c1, c1, c
(17) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace F(a, f(b, f(b, x0))) → c(F(a, f(a, f(b, x0)))) by F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, z0)))))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, z0)))))
S tuples:
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0))))
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, z0)))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c1, c, c
(19) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(a, f(a, z0)))), F(b, f(a, f(a, z0)))) by F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(b, f(b, f(a, z0))))), F(b, f(a, f(a, z0))))
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(b, z0)) → f(a, f(a, f(a, z0)))
f(b, f(a, z0)) → f(b, f(b, f(b, z0)))
Tuples:
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, z0)))))
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(b, f(b, f(a, z0))))), F(b, f(a, f(a, z0))))
S tuples:
F(b, f(a, f(a, x0))) → c1(F(b, f(b, f(a, x0))))
F(a, f(b, f(b, f(b, z0)))) → c(F(a, f(a, f(a, f(a, f(a, f(a, f(a, z0))))))), F(a, f(a, f(a, f(a, f(b, z0))))), F(a, f(b, f(b, z0))))
F(a, f(b, f(b, z0))) → c(F(a, f(a, f(a, f(a, z0)))))
F(b, f(a, f(a, f(a, z0)))) → c1(F(b, f(b, f(b, f(b, f(b, f(b, f(b, z0))))))), F(b, f(b, f(b, f(b, f(a, z0))))), F(b, f(a, f(a, z0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c, c, c1
(21) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
a0() → 0
b0() → 0
f0(0, 0) → 1
(22) BOUNDS(O(1), O(n^1))